COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	%equiva[e89,jmc]		Programming with equivalence relations
C00012 00003	\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
C00013 ENDMK
C⊗;
%equiva[e89,jmc]		Programming with equivalence relations
\input memo.tex[let,jmc]
\title{PROGRAMMING WITH EQUIVALENCE RELATIONS}

\section{The Problem}

	Mathematics provides several ways of building new sets
from old ones.  For example, the rational numbers are built from
the natural numbers in two stages using the cartesian product
operation and forming the set of equivalence classes under
equivalence relations.  Programming languages provide cartesian
product in various guises but don't provide for the formation of sets
of equivalence clases.

	We propose to add a declaration to programming
languages that might take the form

$$declare B = A mod R,$$
%
where $A$ is an already defined type, $R$ is an equivalence
relation on $A$.  This would automatically define a function
$map(A,R)$ such that for $x ε A$, $map(A,R)(x)$ is the
equivalence class to which $x$ belongs.  You can sugar this
notation in different ways if you don't like the notation just
proposed, but that's not the point.

	There's a good reason nothing like this has been
introduced into programming languages.  Doing it requires
giving up something that has always been a part of programming
languages.  Namely, whenever a new way of building types from
older types is proposed, the author has in mind a standard way
of representing elements of the new type in terms of elements
of the old type.  As we shall see, this isn't in general
feasible with equivalence classes.  The point of this paper is
that we should do it anyway and explore how to mitigate the
difficulty.

	Here's an illustration of the problem.  Given ways of
representing members of a set $A$ and members of a set $B$ in the
memory of a computer, there are good standard ways of
representing members of $C = A \times B$.  The implementer of a
compiler for a programming language need only choose one of them.
However, there isn't any standard way of representing members of
equivalence classes.  Consider how the rational numbers are built
up.  We may start in the classical mathemtical way by introducing
the integers.

	Let $N$ be the set of natural numbers.
  We take ordered pairs $<m,n>$ of natural numbers
and introduce the equivalence relation
%
$$<m,n> equiv↓1 <m',n'> ≡ m+n' =m'+n.$$
%
The set $Z$ integers is defined by
%
$$declare Z = (N \times N) mod equiv↓1.$$

	Letting $f = map(N\times N,equiv↓1)$, we define addition
in $Z$ by
%
$$f(<m,n>) + f(<m',n'>) = f(<m+m',n+n'>),$$
%
and to do things properly, we need to prove that $z↓1 + z↓2$
is well defined, i.e. that the equivalence class of the sum
depend only on the equivalence classes of the summands.
The mathematician then goes on to define the other arithmetic
operations on $Z$ and to prove that they have the usual properties.
The relation between the definition in terms of ordered pairs
and the usual notations for integers is discussed informally.

	This is obviously not good enough for programming.  There
are several alternatives,  and all have unpleasant aspects.

First, we can just take arbitrary ordered pairs of natural numbers
as representing integers.  One disadvantage is that the
natural numbers representing integers will tend to grow as calculations
are performed.  Another is that equality is replaced by the
equivalence tests.  The third is that the notation is not
compact.

Second, we can choose a canonical pair as representing the
integer.  In this case it's easy to decide which is best, namely
the pair in which one or the other natural number is 0.  The
disadvantages are that we waste space in memory and that it
isn't clear how a compiler is to choose just this pair.

Third, we can choose the conventional sign-magnitude representation.
It's compact, but the compiler couldn't have chosen it.

This last point becomes even more clear if we consider the
next step in forming the rationals.  A rational is an
equivalence class of ordered pairs of integers, where there
the second element of the pair is positive.  The equivalence
relation is
%
$$<z↓1,z↓2> equiv↓2 <z'↓1,z'↓2> ≡ z↓1z'↓2 = z'↓1z↓2.$$
%
The best representation is fractions in lowest terms.  In
order to hit upon this representation automatically, a compiler
would have to know some elementary number theory, including
the fact that the Euclidean algorithm can be used to reduce
a fraction to lowest terms.

\section{The Proposal}

	We propose to solve the problem in two steps.

	The first step is to ignore the problem.  Consider a programming
language that allows the programmer to use
%
$$declare B = A mod R$$
%
without further ado.  In this language, it is definite how a computation
proceeds and properties of the programs can be proved.  This even
includes properties like the number of computation steps taken,
provided the mappings associated with the equivalence classes
are taken as elementary steps.  The correctness of the program
depends on the alleged equivalence relation being really an
equivalence relation and on the operations on equivalence classes
being well defined if they are defined in terms of operations
involving the basic set.

	The second stage is for the programmer to specify how the
equivalence classes are to be represented and how the operations
on them are to be represented.

	In general the equivalence relations and sets of equivalence
classes will be dynamically defined in blocks.  This is true of the
example problem I have worked with, namely the 15 puzzle.  This
is not the place for the details, but the amount of search in
a program for the 15 puzzle is enormously reduced if positions are
regarded as equivalent under permutations of tiles one is not
currently trying to place.
\smallskip\centerline{Copyright \copyright\ 1989\ by John McCarthy}
\smallskip\noindent{This draft of EQUIVA[E89,JMC]\ TEXed on \jmcdate\ at \theTime}
%File originated on 06-Sep-89
\vfill\eject\end